Handbook of Knowledge Representation
Chapter 2
ruby ではなくて pseudocode だけど syntax highlighting がいい感じになったので
code:ruby
# DPLL(F, ρ)
入力: CNF である論理式 F と初期状態は空の割り当てρ
出力: UNSAT、または F を充足する変数の割り当て
begin
(F, ρ) ← UnitPropagate(F, ρ)
if F が空節を含む then return UNSAT
if F が節を一つも持たない then
ρを出力
return SAT
l ← ρ によって割り当てられていない変数
if DPLL(F|l, ρ∪{l}) = SAT then return SAT
return DPLL(F|¬l, ρ∪{¬l})
end
sub UnitPropagate(F, ρ)
begin
while F が空節を含まず、単位節 x を含むとき do
F ← F|x
ρ ← ρ∪{x}
return (F, ρ)
end
グラフにおける predecessor は parent と同じように捉えてよい
2020-06-14
p98
conflict graph は書いてある通り 3 つの性質を満たすような implication graph の subgraph のことであるが、典型的な実装においては (b), (c) を満たすような subgraph を持っておいて（このグラフのことを unique inference subgraph、固有導出部分グラフ？）、conflict に到達したときに自動的にこの subgraph が (a) を満たすようになるので、結果的に conflict graph としての性質を全て満たすようになる。
p99 まで読んだ
ある頂点の集合 U があったとき、 U の edge-cut（以降はカットと呼ぶ）は$ v_{\in U} \longrightarrow v_{\notin U} を満たすような辺を集めたもののこと。
cause of the conflict は、$ v_{\texttt{reason}} \longrightarrow v_{\texttt{conflict}} を満たすような辺が一つ以上あるようなすべての$ v_{\texttt{reason}}たちによって形成される。
カットにはいろいろある
カットの仕方のことを learning scheme と呼んでいる
カットとして選ぶのは、その辺に対応するような clause がまだ known clause でなかったようなものである。
Handbook では conflict から学習するのはただ一つの clause であると簡単のために仮定している。
p101 に resolution の話が載ってた……
ただの resolution のことを、general resolution と呼んでいるっぽい
証明戦略にはいろいろある
ただの resolution だけだと、tree-like, regular, and ordered resolution などよりも exponentially stronger で、非効率
tree-like resolution は、regular, ordered, linear, positive, negative, and semantic resolution よりも exponentially weaker で、効率がよい
だから、tree-like resolution が実装上はよろしいのかな
訳（退避）
Clause Learning で出てくるもの
Implication graph, conflict graph
Implication graph の定義
各頂点はリテラルが乗っていて、辺には節がラベル付けされている
decision literal については、入次数が 0 の頂点になる
その implication graph に $ \lnot l_1, \lnot l_2, \cdots, \lnot l_kの頂点があって、現在既知である clause $ C = (l_1 \lor l_2 \lor \cdots \lor l_k \lor l)があるとき、
1. graph に 頂点として$ lを追加
2. $ 1 \le i \le kについて、有向辺$ (\lnot l_i, l) を追加
3. これらの辺に節$ Cをラベル付けする。すると、それらの辺は節$ Cと結びつき、グループとして扱うことができる。
その implication graph に特別な「conflict」を表す頂点$ \overline \Lambdaを追加する。その implication graph において真、偽のどちらでも現れるような変数$ xについて、$ x, \lnot xそれぞれから$ \overline \Lambdaに向かうような辺を追加する。
implication graph の性質
DAG
すべての頂点にラベル付けされたものは互いに異なるので、リテラルのみで頂点を区別することができる。
implication graph である G にconflict があるのは、それが少なくとも一つの conflict 変数を持つときである。Unit Propagate などによって空節$ \Lambdaが残ったときはこれと等価であるといえる。
$ \overline \Lambdaは implication graph 上の、conflict を表現する頂点を表す。
$ \Lambdaは、空節を表す。
implication graph の定義からすると、このグラフには一つも conflict がない場合もあれば、大量の conflict を含んだり、一つのリテラルをとっても導出方法は複数個存在する場合がある。ここで、より理解しやすくする、また、いつどのように conflict が起きるのか分析しやすくするために、implication graph の部分グラフである "conflict graph" について考える。これは、unit propagation を用いることによって decision variables から conflict にまで辿りつくための考えうる大量の方法から、たった一つのみを捉えるようになっているグラフである。
conflict graph の定義
conflict graph は、下記の性質を満たすような、implication graph の任意の部分グラフのことである。
1. そのグラフには$ \overline \Lambdaが含まれており、ただ一つの conflict 変数が含まれる。
2. そのグラフのすべての頂点から、$ \overline \Lambdaへの道が存在する。
3. $ \overline \Lambda以外のすべての頂点$ lは decision literal であるか、または$ (l_1 \lor l_2 \lor \dots \lor l_k \lor l)という節が既知であるとき、$ \lnot l_1, \lnot l_2, \cdots, \lnot l_kたちを一つ前の頂点として（しかもこれらに限って）持つ。
conflict graph の性質
implication graph は conflict を持つかもしれないし持たないかもしれない。しかし、conflict graph はいつだってただ一つの conflict を持つ。
conflict graph の選び方はそのソルバーの戦略の一部である。（ソルバに委ねられる）
典型的なやり方では、2. と 3. を満たすような implication graph の部分グラフを持っておいて（この部分グラフのことを unique inference subgraph という）、conflict に到達したときにこれを 1. も満たすようにすることで、結果的に conflict graph ができあがる。そして、これによって conflict を分析することができるようになる、といった寸法である。